abstract class $ARR{ETP} < $RO_ARR{ETP}
****
The indices are integers and lie in [0, size-1] Similar to a MAP from ints to elements, but more restrictive conditions The features are repeated here so as to restate the preconditions Inherits: copy, size, capacity, elt! and has size: INT; elt!: ETP; has(e: ETP): BOOL;


Ancestors
$RO_ARR{_} $CONTAINER{_} $ELT{_} $ELT

Descendants
ARRAY{_} AM_CALL_EXPR AM_ITER_CALL_EXPR AM_EXT_CALL_EXPR
AM_BND_ROUT_CALL_EXPR AM_BND_ITER_CALL_EXPR AM_ROUT_CALL_EXPR LAYOUT_ARRAY
AM_BND_CREATE_EXPR AM_ARRAY_EXPR AM_ROUT_DEF CODE_FILE_ARRAY
LAYOUT_ARR TP_ARRAY FLIST{_} FSTR



Public


Features
aget(i: INT): ETP;
**** pre has_ind(i)
aset(ind: INT,e: ETP);
**** pre has_ind(i)
copy: $ARR{ETP};
**** Redefined to narrow the return type
has_ind(i: INT): BOOL;
**** return 0<=i<size This method could actually be implemented at this level
ind!: INT;
**** post 0<=result<size Returns all the indices, which are the integers between 0 and size - 1